\section{B Method}

\begin{frame}
\hypertarget{metodoB}{}
  \frametitle{B Method} 
  \begin{itemize}
    \item B method for software development is a formal method based on
	    \begin{itemize}
	    \item  B Abstract Machine Notation (AMN)
	    \item  First order logic, integer arithmetic and set theory
	    \end{itemize}
    \item It is similar to the Z notation
%     \begin{itemize} \item But it has also the substitution calculus and the
%     refinement calculus
%     \end{itemize}   
    \item Supports:
    \begin{itemize}
	    \item Modularization
	    \item Advanced techniques for proof development: user pass,
	    parallelization, etc.
	    \item Refinements proved up to basic constructs of programming language  
	    \item Code generator to programming language
	    \item \ldots
    \end{itemize}   
  \end{itemize}
\end{frame}
    
    
%     
% \begin{frame}
% \frametitle{B Method- Simple example}
% \begin{figure}
%   % \begin{small}
%   $$
%   \begin{array}{lcl}
%     \begin{array}[t]{l}
%       \MACHINE \\ \quad  \mathit{micro} \\
%       \SEES \\ \quad \mathit{TYPES}, \mathit{ALU} \\
%       \INCLUDES \\  \quad \mathit{MEMORY} \\
%       \VARIABLES \\ \quad    \mathit{pc}  \\
%       \INVARIANT \\ \quad \mathit{pc} \in \mathit{INSTRUCTION} 
%     \end{array}
%     & \hspace*{0cm} &
%     \begin{array}[t]{l}
%       \INITIALISATION  \mathit{pc} := 0 \\
%       \OPERATIONS\\
%       \mathit{JMP} \mathit{( jump )} = \\
%       \quad \PRE \mathit{jump} \in \mathit{INSTRUCTION}\\ 
%       \quad \THEN \mathit{pc} := \mathit{jump}\\  
%       \quad \END \\
%       \END
%     \end{array}
%   \end{array}
%   $$
% \caption{A very basic B machine.}
% \label{fig:maqB}
% \end{figure}
% \end{frame}